Search

As robots become more prevalent, the complexity of robot-robot, robot-human, and robot-environment interactions increases. In these interactions, a robot needs to consider not only the effects of its own actions, but also the effects of other agents' actions and the possible interactions between agents. Previous works have considered reactive synthesis, where the human/environment is modeled as a deterministic, adversarial agent; as well as probabilistic synthesis, where the human/environment is modeled via a Markov chain. While they provide strong theoretical frameworks, there are still many aspects of human-robot interaction that cannot be fully expressed and many assumptions that must be made in each model. In this work, we propose stochastic games as a general model for human-robot interaction, which subsumes the expressivity of all previous representations. In addition, it allows us to make fewer modeling assumptions and leads to more natural and powerful models of interaction. We introduce the semantics of this abstraction and show how existing tools can be utilized to synthesize strategies to achieve complex tasks with guarantees. Further, we discuss the current computational limitations and improve the scalability by two orders of magnitude by a new way of constructing models for PRISM-games., Comment: Accepted: ICRA 2024

We introduce a method for translating an alternating weak B\"uchi automaton (AWA), which corresponds to a Linear Dynamic Logic (LDL) formula, to an unambiguous B\"uchi automaton (UBA). Our translations generalise constructions for Linear Temporal Logic (LTL), a less expressive specification language than LDL. In classical constructions, LTL formulas are first translated to alternating \emph{very weak} automata (AVAs) -- automata that have only singleton strongly connected components (SCCs); the AVAs are then handled by efficient disambiguation procedures. However, general AWAs can have larger SCCs, which complicates disambiguation. Currently, the only available disambiguation procedure has to go through an intermediate construction of nondeterministic B\"uchi automata (NBAs), which would incur an exponential blow-up of its own. We introduce a translation from \emph{general} AWAs to UBAs with a \emph{singly} exponential blow-up, which also immediately provides a singly exponential translation from LDL to UBAs. Interestingly, the complexity of our translation is \emph{smaller} than the best known disambiguation algorithm for NBAs (broadly $(0.53n)^n$ vs. $(0.76n)^n$), while the input of our construction can be exponentially more succinct., Comment: 23 pages

The innovations in reactive synthesis from {\em Linear Temporal Logics over finite traces} (LTLf) will be amplified by the ability to verify the correctness of the strategies generated by LTLf synthesis tools. This motivates our work on {\em LTLf model checking}. LTLf model checking, however, is not straightforward. The strategies generated by LTLf synthesis may be represented using {\em terminating} transducers or {\em non-terminating} transducers where executions are of finite-but-unbounded length or infinite length, respectively. For synthesis, there is no evidence that one type of transducer is better than the other since they both demonstrate the same complexity and similar algorithms. In this work, we show that for model checking, the two types of transducers are fundamentally different. Our central result is that LTLf model checking of non-terminating transducers is \emph{exponentially harder} than that of terminating transducers. We show that the problems are EXPSPACE-complete and PSPACE-complete, respectively. Hence, considering the feasibility of verification, LTLf synthesis tools should synthesize terminating transducers. This is, to the best of our knowledge, the \emph{first} evidence to use one transducer over the other in LTLf synthesis., Comment: Accepted by ATVA 23

In the study of reactive systems, qualitative properties are usually easier to model and analyze than quantitative properties. This is especially true in systems where mutually beneficial cooperation between agents is possible, such as multi-agent systems. The large number of possible payoffs available to agents in reactive systems with quantitative properties means that there are many scenarios in which agents deviate from mutually beneficial outcomes in order to gain negligible payoff improvements. This behavior often leads to less desirable outcomes for all agents involved. For this reason we study satisficing goals, derived from a decision-making approach aimed at meeting a good-enough outcome instead of pure optimization. By considering satisficing goals, we are able to employ efficient automata-based algorithms to find pure-strategy Nash equilibria. We then show that these algorithms extend to scenarios in which agents have multiple thresholds, providing an approximation of optimization while still retaining the possibility of mutually beneficial cooperation and efficient automata-based algorithms. Finally, we demonstrate a one-way correspondence between the existence of $\epsilon$-equilibria and the existence of equilibria in games where agents have multiple thresholds., Comment: Preliminary version of the technical report for a paper to appear in IJCAI'23

Determining the satisfiability of Boolean constraint-satisfaction problems with different types of constraints, that is hybrid constraints, is a well-studied problem with important applications. We study here a new application of hybrid Boolean constraints, which arises in quantum computing. The problem relates to constrained perfect matching in edge-colored graphs. While general-purpose hybrid constraint solvers can be powerful, we show that direct encodings of the constrained-matching problem as hybrid constraints scale poorly and special techniques are still needed. We propose a novel encoding based on Tutte's Theorem in graph theory as well as optimization techniques. Empirical results demonstrate that our encoding, in suitable languages with advanced SAT solvers, scales significantly better than a number of competing approaches on constrained-matching benchmarks. Our study identifies the necessity of designing problem-specific encodings when applying powerful general-purpose constraint solvers., Comment: Accepted by IJCAI'23

While the Ising model remains essential to understand physical phenomena, its natural connection to combinatorial reasoning makes it also one of the best models to probe complex systems in science and engineering. We bring a computational lens to the study of Ising models, where our computer-science perspective is two-fold: On the one hand, we consider the computational complexity of the Ising partition-function problem, or #Ising, and relate it to the logic-based counting of constraint-satisfaction problems, or #CSP. We show that known dichotomy results for #CSP give an easy proof of the hardness of #Ising and provide new intuition on where the difficulty of #Ising comes from. On the other hand, we also show that #Ising can be reduced to Weighted Model Counting (WMC). This enables us to take off-the-shelf model counters and apply them to #Ising. We show that this WMC approach outperforms state-of-the-art specialized tools for #Ising, thereby expanding the range of solvable problems in computational physics., Comment: 16 pages, 2 figures

We propose and study the graph-theoretical problem EXISTS-PMVC: the existence of perfect matching under vertex-color constraints on graphs with bi-colored edges. EXISTS-PMVC is of special interest because of its motivation from quantum-state identification and quantum-experiment design, as well as its rich expressiveness, i.e., EXISTS-PMVC naturally subsumes important constrained matching problems, such as exact perfect matching. We give complexity and algorithmic results for EXISTS-PMVC under two types of vertex color constraints: (1) decision-diagram constraints (EXISTS-PMVC-DD) and (2) symmetric constraints (EXISTS-PMVC-Sym). For EXISTS-PMVC-DD, we reveal its NP-hardness by a graph-gadget technique. We prove that EXISTS-PMVC-Sym with a bounded number of colors (EXISTS-PMVC-Sym-Bounded) is polynomially equivalent with Exact Perfect Matching (XPM), which implies that EXISTS-PMVC-Sym-Bounded is in RNC on general graphs and PTIME on planar graphs. Directly applying algorithms for XPM to solve EXISTS-PMVC-Sym-Bounded is, however, impractical. We propose algorithms that natively handle EXISTS-PMVC-Sym-Bounded with considerably better complexity. Our novel results for EXISTS-PMVC provide insights into both constrained matching and scalable quantum experiment design., Comment: 13 pages excluding appendix and reference. 4 figures

The determinization of a nondeterministic B\"uchi automaton (NBA) is a fundamental construction of automata theory, with applications to probabilistic verification and reactive synthesis. The standard determinization constructions, such as the ones based on the Safra-Piterman's approach, work on the whole NBA. In this work we propose a divide-and-conquer determinization approach. To this end, we first classify the strongly connected components (SCCs) of the given NBA as inherently weak, deterministic accepting, and nondeterministic accepting. We then present how to determinize each type of SCC independently from the others; this results in an easier handling of the determinization algorithm that takes advantage of the structure of that SCC. Once all SCCs have been determinized, we show how to compose them so to obtain the final equivalent deterministic Emerson-Lei automaton, which can be converted into a deterministic Rabin automaton without blow-up of states and transitions. We implement our algorithm in a our tool COLA and empirically evaluate COLA with the state-of-the-art tools Spot and OWL on a large set of benchmarks from the literature. The experimental results show that our prototype COLA outperforms Spot and OWL regarding the number of states and transitions., Comment: This is an extended version of our CAV'22 paper

Reactive synthesis from high-level specifications that combine hard constraints expressed in Linear Temporal Logic LTL with soft constraints expressed by discounted-sum (DS) rewards has applications in planning and reinforcement learning. An existing approach combines techniques from LTL synthesis with optimization for the DS rewards but has failed to yield a sound algorithm. An alternative approach combining LTL synthesis with satisficing DS rewards (rewards that achieve a threshold) is sound and complete for integer discount factors, but, in practice, a fractional discount factor is desired. This work extends the existing satisficing approach, presenting the first sound algorithm for synthesis from LTL and DS rewards with fractional discount factors. The utility of our algorithm is demonstrated on robotic planning domains.

In Bayesian inference, the maximum a posteriori (MAP) problem combines the most probable explanation (MPE) and marginalization (MAR) problems. The counterpart in propositional logic is the exist-random stochastic satisfiability (ER-SSAT) problem, which combines the satisfiability (SAT) and weighted model counting (WMC) problems. Both MAP and ER-SSAT have the form $\operatorname{argmax}_X \sum_Y f(X, Y)$, where $f$ is a real-valued function over disjoint sets $X$ and $Y$ of variables. These two optimization problems request a value assignment for the $X$ variables that maximizes the weighted sum of $f(X, Y)$ over all value assignments for the $Y$ variables. ER-SSAT has been shown to be a promising approach to formally verify fairness in supervised learning. Recently, dynamic programming on graded project-join trees has been proposed to solve weighted projected model counting (WPMC), a related problem that has the form $\sum_X \max_Y f(X, Y)$. We extend this WPMC framework to exactly solve ER-SSAT and implement a dynamic-programming solver named DPER. Our empirical evaluation indicates that DPER contributes to the portfolio of state-of-the-art ER-SSAT solvers (DC-SSAT and erSSAT) through competitive performance on low-width problem instances., Comment: arXiv admin note: substantial text overlap with arXiv:2205.08632

In Bayesian inference, the most probable explanation (MPE) problem requests a variable instantiation with the highest probability given some evidence. Since a Bayesian network can be encoded as a literal-weighted CNF formula $\varphi$, we study Boolean MPE, a more general problem that requests a model $\tau$ of $\varphi$ with the highest weight, where the weight of $\tau$ is the product of weights of literals satisfied by $\tau$. It is known that Boolean MPE can be solved via reduction to (weighted partial) MaxSAT. Recent work proposed DPMC, a dynamic-programming model counter that leverages graph-decomposition techniques to construct project-join trees. A project-join tree is an execution plan that specifies how to conjoin clauses and project out variables. We build on DPMC and introduce DPO, a dynamic-programming optimizer that exactly solves Boolean MPE. By using algebraic decision diagrams (ADDs) to represent pseudo-Boolean (PB) functions, DPO is able to handle disjunctive clauses as well as XOR clauses. (Cardinality constraints and PB constraints may also be compactly represented by ADDs, so one can further extend DPO's support for hybrid inputs.) To test the competitiveness of DPO, we generate random XOR-CNF formulas. On these hybrid benchmarks, DPO significantly outperforms MaxHS, UWrMaxSat, and GaussMaxHS, which are state-of-the-art exact solvers for MaxSAT.

Boolean MaxSAT, as well as generalized formulations such as Min-MaxSAT and Max-hybrid-SAT, are fundamental optimization problems in Boolean reasoning. Existing methods for MaxSAT have been successful in solving benchmarks in CNF format. They lack, however, the ability to handle 1) (non-CNF) hybrid constraints, such as XORs and 2) generalized MaxSAT problems natively. To address this issue, we propose a novel dynamic-programming approach for solving generalized MaxSAT problems with hybrid constraints -- called \emph{Dynamic-Programming-MaxSAT} or DPMS for short -- based on Algebraic Decision Diagrams (ADDs). With the power of ADDs and the (graded) project-join-tree builder, our versatile framework admits many generalizations of CNF-MaxSAT, such as MaxSAT, Min-MaxSAT, and MinSAT with hybrid constraints. Moreover, DPMS scales provably well on instances with low width. Empirical results indicate that DPMS is able to solve certain problems quickly, where other algorithms based on various techniques all fail. Hence, DPMS is a promising framework and opens a new line of research that invites more investigation in the future.

The problems of \emph{verification} and \emph{realizability} are two central themes in the analysis of reactive systems. When multiagent systems are considered, these problems have natural analogues of existence (nonemptiness) of pure-strategy Nash equilibria and verification of pure-strategy Nash equilibria. Recently, this body of work has begun to include finite-horizon temporal goals. With finite-horizon temporal goals, there is a natural hierarchy of goal representation, ranging from deterministic finite automata (DFA), to nondeterministic finite automata (NFA), and to alternating finite automata (AFA), with a worst-case exponential gap between each successive representation. Previous works showed that the realizability problem with DFA goals was PSPACE-complete, while the realizability problem with temporal logic goals is in 2EXPTIME. In this work, we study both the realizability and the verification problems with respect to various goal representations. We first show that the realizability problem with NFA goals is EXPTIME-complete and with AFA goals is 2EXPTIME-complete, thus establishing strict complexity gaps between realizability with respect to DFA, NFA, and AFA goals. We then contrast these complexity gaps with the complexity of the verification problem, where we show that verification with respect to DFAs, NFA, and AFA goals is PSPACE-complete., Comment: Technical report for a KR 2022 paper

In this work, we exploit the power of \emph{finite ambiguity} for the complementation problem of B\"uchi automata by using reduced run directed acyclic graphs (DAGs) over infinite words, in which each vertex has at most one predecessor; these reduced run DAGs have only a finite number of infinite runs, thus obtaining the finite ambiguity in B\"uchi complementation. We show how to use this type of reduced run DAGs as a unified tool to optimize both rank-based and slice-based complementation constructions for B\"uchi automata with a finite degree of ambiguity. As a result, given a B\"uchi automaton with $n$ states and a finite degree of ambiguity, the number of states in the complementary B\"uchi automaton constructed by the classical rank-based and slice-based complementation constructions can be improved from $2^{\mathsf{O}(n \log n)}$ and $\mathsf{O}((3n)^{n})$ to $\mathsf{O}(6^{n}) \subseteq 2^{\mathsf{O}(n)}$ and $\mathsf{O}(4^{n})$, respectively. We further show how to construct such reduced run DAGs for limit deterministic B\"uchi automata and obtain a specialized complementation algorithm, thus demonstrating the generality of the power of finite ambiguity.

Temporal logics are widely used by the Formal Methods and AI communities. Linear Temporal Logic is a popular temporal logic and is valued for its ease of use as well as its balance between expressiveness and complexity. LTL is equivalent in expressiveness to Monadic First-Order Logic and satisfiability for LTL is PSPACE-complete. Linear Dynamic Logic (LDL), another temporal logic, is equivalent to Monadic Second-Order Logic, but its method of satisfiability checking cannot be applied to a nontrivial subset of LDL formulas. Here we introduce Automata Linear Dynamic Logic on Finite Traces (ALDL_f) and show that satisfiability for ALDL_f formulas is in PSPACE. A variant of Linear Dynamic Logic on Finite Traces (LDL_f), ALDL_f combines propositional logic with nondeterministic finite automata (NFA) to express temporal constraints. ALDL$_f$ is equivalent in expressiveness to Monadic Second-Order Logic. This is a gain in expressiveness over LTL at no cost.

In the \emph{Adapter Design Pattern}, a programmer implements a \emph{Target} interface by constructing an \emph{Adapter} that accesses an existing \emph{Adaptee} code. In this work, we present a reactive synthesis interpretation to the adapter design pattern, wherein an algorithm takes an \emph{Adaptee} and a \emph{Target} transducers, and the aim is to synthesize an \emph{Adapter} transducer that, when composed with the {\em Adaptee}, generates a behavior that is equivalent to the behavior of the {\em Target}. One use of such an algorithm is to synthesize controllers that achieve similar goals on different hardware platforms. While this problem can be solved with existing synthesis algorithms, current state-of-the-art tools fail to scale. To cope with the computational complexity of the problem, we introduce a special form of specification format, called {\em Separated GR($k$)}, which can be solved with a scalable synthesis algorithm but still allows for a large set of realistic specifications. We solve the realizability and the synthesis problems for Separated GR($k$), and show how to exploit the separated nature of our specification to construct better algorithms, in terms of time complexity, than known algorithms for GR($k$) synthesis. We then describe a tool, called SGR($k$), that we have implemented based on the above approach and show, by experimental evaluation, how our tool outperforms current state-of-the-art tools on various benchmarks and test-cases.

We revisit here congruence relations for B\"uchi automata, which play a central role in the automata-based verification. The size of the classical congruence relation is in $3^{\mathcal{O}(n^2)}$, where $n$ is the number of states of a given B\"uchi automaton $\mathcal{A}$. Here we present improved congruence relations that can be exponentially coarser than the classical one. We further give asymptotically optimal congruence relations of size $2^{\mathcal{O}(n \log n)}$. Based on these optimal congruence relations, we obtain an optimal translation from B\"uchi automata to a family of deterministic finite automata (FDFW) that accepts the complementary language. To the best of our knowledge, our construction is the first direct and optimal translation from B\"uchi automata to FDFWs.

Several problems in planning and reactive synthesis can be reduced to the analysis of two-player quantitative graph games. {\em Optimization} is one form of analysis. We argue that in many cases it may be better to replace the optimization problem with the {\em satisficing problem}, where instead of searching for optimal solutions, the goal is to search for solutions that adhere to a given threshold bound. This work defines and investigates the satisficing problem on a two-player graph game with the discounted-sum cost model. We show that while the satisficing problem can be solved using numerical methods just like the optimization problem, this approach does not render compelling benefits over optimization. When the discount factor is, however, an integer, we present another approach to satisficing, which is purely based on automata methods. We show that this approach is algorithmically more performant -- both theoretically and empirically -- and demonstrates the broader applicability of satisficing overoptimization., Comment: arXiv admin note: text overlap with arXiv:2010.02055

The problem of finding pure strategy Nash equilibria in multiagent concurrent games with finite-horizon temporal goals has received some recent attention. Earlier work solved this problem through the use of Rabin automata. In this work, we take advantage of the finite-horizon nature of the agents' goals and show that checking for and finding pure strategy Nash equilibria can be done using a combination of safety games and lasso testing in B\"uchi automata. To separate strategic reasoning from temporal reasoning, we model agents' goals by deterministic finite-word automata (DFAs), since finite-horizon logics such as LTL\textsubscript{f} and LDL\textsubscript{f} are reasoned about through conversion to equivalent DFAs. This allow us characterize the complexity of the problem as PSPACE complete., Comment: Technical report for an AAMAS 2021 paper v2 - cleaned up typos, fixed some bugs

We explore the potential of continuous local search (CLS) in SAT solving by proposing a novel approach for finding a solution of a hybrid system of Boolean constraints. The algorithm is based on CLS combined with belief propagation on binary decision diagrams (BDDs). Our framework accepts all Boolean constraints that admit compact BDDs, including symmetric Boolean constraints and small-coefficient pseudo-Boolean constraints as interesting families. We propose a novel algorithm for efficiently computing the gradient needed by CLS. We study the capabilities and limitations of our versatile CLS solver, GradSAT, by applying it on many benchmark instances. The experimental results indicate that GradSAT can be a useful addition to the portfolio of existing SAT and MaxSAT solvers for solving Boolean satisfiability and optimization problems., Comment: AAAI 21

The matrix permanent belongs to the complexity class #P-Complete. It is generally believed to be computationally infeasible for large problem sizes, and significant research has been done on approximation algorithms for the matrix permanent. We present an implementation and detailed runtime analysis of one such Markov Chain Monte Carlo (MCMC) based Fully Polynomial Randomized Approximation Scheme (FPRAS) for the matrix permanent, which has previously only been described theoretically and with big-Oh runtime analysis. We demonstrate by analysis and experiment that the constant factors hidden by previous big-Oh analyses result in computational infeasibility., Comment: This article is based on an MS thesis by the first author, submitted to Rice University on June 12, 2020. Research partially supported by NSF Grant no. IIS-1527668